[[R]]
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> @loc: x:T
== Rinit(loc,T,x,v)=> @loc: xinitially x = v
== Rframe(loc,T,x,L)=> @loc: only L affects x : T
== Rsframe(lnk,tag,L)=> @source(lnk): only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,f)=> @loc: with declarations 
== ds:ds
== da:knd : T

== effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> @source(l): with declarations 
== ds:ds
== da:knd : T  lnk-decl(l;dt)
== dknd(v) sends g s v on link l
== Rpre(loc,ds,a,T,P)=> @loc (with ds: ds
== Rpre(loc,ds,a,T,P)=> @loc action a:T
== Rpre(loc,ds,a,T,P)=> @loc precondition a(v) is
== Rpre(loc,ds,a,T,P)=> @loc P s v)
== Raframe(loc,k,L)=> @loc: k affects only members of L
== Rbframe(loc,k,L)=> @loc: k sends only links in L
== Rrframe(loc,x,L)=> @loc: only members of L read x 

latex

---

clarification:

[[R]]
== case R of 
== Rnone => 
== Rplus(left,right)=>rec1,rec2.rec1  rec2
== Rinit(loc,T,x,v)=> @loc: x:T
== Rinit(loc,T,x,v)=> @loc: xinitially x = v
== Rframe(loc,T,x,L)=> @loc: only L affects x : T
== Rsframe(lnk,tag,L)=> @source(lnk): only L sends on (lnk with tag)
== Reffect(loc,ds,knd,T,x,f)=> @loc: with declarations 
== ds:ds
== da:knd : T

== effect of knd(v) is x := f s v
== Rsends(ds,knd,T,l,dt,g)=> @source(l): with declarations 
== ds:ds
== da:fpf-join(KindDeq;knd : T;lnk-decl(l;dt))
== dknd(v) sends g s v on link l
== Rpre(loc,ds,a,T,P)=> @loc (with ds: ds
== Rpre(loc,ds,a,T,P)=> @loc action a:T
== Rpre(loc,ds,a,T,P)=> @loc precondition a(v) is
== Rpre(loc,ds,a,T,P)=> @loc P s v)
== Raframe(loc,k,L)=> @loc: k affects only members of L
== Rbframe(loc,k,L)=> @loc: k sends only links in L
== Rrframe(loc,x,L)=> @loc: only members of L read x 

latex

Definitions

es realizer ind, , A  B, @i: x:T initially x = v, @i: only L affects x : t, @i: only L sends on (l with tg), @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, @i: with declarations ds:dsda:da k(v) sends f s v on link l, source(l), f  g, KindDeq, x : v, lnk-decl(l;dt), @i (with ds: ds action a:T precondition a(v) is P s v), @i: k affects only members of L, @i: k sends only links in L, @i: only members of L read x

FDL editor aliases

R-Dsys